Interleaving bisimulation semantics

In this section we will show that interleaving bisimulation equivalence [Park, Milner] is preserved under safe refinements.

Definition 4.1  
 A relation R⊆$\it Conf\/$($\cal {E}$)×$\it Conf\/$($\cal {F}$) is called an interleaving bisimulation between $\cal {E}$ and $\cal {F}$ iff (∅,∅)∈R, and if (X, Y)∈R then
  • X$\buildrel$a$\over$→X'⇒∃Y' with Y$\buildrel$a$\over$→Y' and (X', Y')∈R,
  • Y$\buildrel$a$\over$→Y'⇒∃X' with X$\buildrel$a$\over$→X' and (X', Y')∈R.
$\cal {E}$ and $\cal {F}$ are interleaving bisimulation equivalent ( $\cal {E}$ $\approx_{{ib}}^{}$ $\cal {F}$) iff there exists an interleaving bisimulation between $\cal {E}$ and $\cal {F}$ .

In [GG a] it has been shown that the configurations of a refined event structure may be deduced compositionally from the configurations of the original event structure and those of the refinements of actions. We will use this result and the following lemmas in the proof of the refinement theorem.

Definition 4.2  
 
(i) We call $\tilde{X}$ a refinement of a configuration X∈$\it Conf\/$($\cal {E}$) by $\it ref\/$ iff
-  $\tilde{X}$ = $\bigcup\limits_{{e \in X}}^{}$({e}×Xe) where ∀e∈X : Xe∈$\it Conf\/$($\it ref\/$(l$\scriptstyle \cal {E}$(e))) - {∅},
-  busy($\tilde{X}$)⊆max(X) where
  • max(X) denotes the set of all maximal events in X w.r.t. < X,
  • busy($\tilde{X}$) : = X - compl ($\tilde{X}$) and
  • compl ($\tilde{X}$) : = {e∈X | Xe is a complete configuration}.
(ii)  $\it ref\/$(X) denotes the set of refinements of X∈$\it Conf\/$($\cal {E}$) by ref
and for S⊆$\it Conf\/$($\cal {E}$), $\it ref\/$(S) = $\displaystyle \bigcup_{{X \in S}}^{}$$\displaystyle \it ref\/$(X).

Clearly, if $\tilde{X}$∈$\it ref\/$(X) then X = pr($\tilde{X}$) : = {e∈E$\scriptstyle \cal {E}$ | ∃e'∈E$\scriptstyle \it ref\/$(l(e)) : (e, e')∈$\tilde{X}$} and we have compl ($\tilde{X}$)⊆pr($\tilde{X}$), pr($\tilde{X}$) - max(pr($\tilde{X}$))⊆compl ($\tilde{X}$).

Proposition 4.1  
 Then $\it Conf\/$($\it ref\/$($\cal {E}$)) = $\it ref\/$($\it Conf\/$($\cal {E}$)).

Lemma 4.1  
 If compl ($\tilde{X}$)⊆Y⊆pr($\tilde{X}$) then Y∈$\it Conf\/$($\cal {E}$).

Proof Immediate from proposition [*](iii), since pr($\tilde{X}$) - max(pr($\tilde{X}$))⊆Y⊆pr($\tilde{X}$). $\Box$

With lemma [*] we have in particular compl ($\tilde{X}$)∈$\it Conf\/$($\cal {E}$).

Lemma 4.2  
  X$\buildrel$a$\over$→X1, X$\buildrel$a$\over$→X2⇒X1 = X2.

Proof Immediate from the definitions. $\Box$

Lemma 4.3  
 If e∈pr($\tilde{X}$) - compl ($\tilde{X}$) then l$\scriptstyle \cal {E}$(e) $\not\in$Crit$\scriptstyle \cal {E}$.

Proof With proposition [*] we have Xe∈$\it Conf\/$($\it ref\/$(l$\scriptstyle \cal {E}$(e))) - {∅}.
If l$\scriptstyle \cal {E}$(e)∈Crit$\scriptstyle \cal {E}$ than Xe is complete by proposition [*].
However, since e∈pr($\tilde{X}$) - compl ($\tilde{X}$), Xe is not complete. $\Box$

Lemma 4.4  
 If compl ($\tilde{X}$)∪{e}∈$\it Conf\/$($\cal {E}$) then pr($\tilde{X}$)∪{e}∈$\it Conf\/$($\cal {E}$).

Proof W.l.o.g. we assume that e $\not\in$pr($\tilde{X}$).
With proposition [*](i) we prove that pr($\tilde{X}$) enables e.

Suppose ∃d∈pr($\tilde{X}$) with d#e. Since compl ($\tilde{X}$)∪{e} is conflict-free, it follows that d∈pr($\tilde{X}$) - compl ($\tilde{X}$). Thus compl ($\tilde{X}$) enables d (with lemma [*]) as well as e, so d ch e. However, with lemma [*] we have l (d ) $\not\in$Crit$\scriptstyle \cal {E}$, contradicting d ch e.

Now suppose d $\prec$ e and d $\not\in$pr($\tilde{X}$)⊇compl ($\tilde{X}$). Since compl ($\tilde{X}$)∪{e}∈$\it Conf\/$($\cal {E}$) there is an f∈compl ($\tilde{X}$)⊆pr($\tilde{X}$) with f $\prec$ e and d#f. $\Box$

With these lemmas we can prove the theorem.

Theorem 4.1  
 Then     $\cal {E}$ $\approx_{{ib}}^{}$ $\cal {F}$    ⇒    $\it ref\/$($\cal {E}$) $\approx_{{ib}}^{}$ $\it ref\/$($\cal {F}$).

Proof Let R be a bisimulation between $\cal {E}$ and $\cal {F}$.
Let $\tilde{R}$ = {($\tilde{X}$,$\tilde{Y}$)∈$\it Conf\/$($\it ref\/$($\cal {E}$))×$\it Conf\/$($\it ref\/$($\cal {F}$)) |
(compl ($\tilde{X}$), compl ($\tilde{Y}$))∈R,
there exist bijections f : pr($\tilde{X}$)→pr($\tilde{Y}$) with l$\scriptstyle \cal {F}$(f (e)) = l$\scriptstyle \cal {E}$(e)
and $\tilde{f}$ : $\tilde{X}$→$\tilde{Y}$ with $\tilde{f}$(e, e') = (f (e), e')}

We show that $\tilde{R}$ is a bisimulation between $\it ref\/$($\cal {E}$) and $\it ref\/$($\cal {F}$).

i. Obviously (∅,∅)∈$\tilde{R}$.

ii. Let ($\tilde{X}$,$\tilde{Y}$)∈$\tilde{R}$. Then (compl ($\tilde{X}$), compl ($\tilde{Y}$))∈R and there are bijections f and $\tilde{f}$ as required in the definition of $\tilde{R}$. We have to show the bisimulation properties. It suffices to check one of them, the other follows by symmetry.

Let $\tilde{X}$$\buildrel$a$\over$→$\tilde{X}{^\prime}$. Let $\tilde{X}{^\prime}$ - $\tilde{X}$ = {(eo, e*)}, l$\scriptstyle \cal {E}$(eo) = b. Then l$\scriptstyle \it ref\/$($\scriptstyle \cal {E}$)((eo, e*)) = l$\scriptstyle \it ref\/$(b)(e*) = a.
Now we have to show : ∃$\tilde{Y}{^\prime}$∈$\it Conf\/$($\it ref\/$($\cal {F}$)) with $\tilde{Y}$$\buildrel$a$\over$→$\tilde{Y}{^\prime}$ and ($\tilde{X}{^\prime}$,$\tilde{Y}{^\prime}$)∈$\tilde{R}$.
For the construction of $\tilde{Y}{^\prime}$, we distinguish two cases.



1. pr($\tilde{X}{^\prime}$) = pr($\tilde{X}$).

In this case we can use the bijection f to define $\tilde{Y}{^\prime}$, since its domain is not affected by adding the new event.

Let $\tilde{Y}{^\prime}$ : = {(f (e), e') | (e, e')∈$\tilde{X}{^\prime}$}.
With $\tilde{Y}$ = {(f (e), e') | (e, e')∈$\tilde{X}$} we have $\tilde{Y}{^\prime}$ = $\tilde{Y}$∪{(f (eo), e*)}.

First we show that $\tilde{Y}{^\prime}$ is a configuration with $\tilde{Y}$$\buildrel$a$\over$→$\tilde{Y}{^\prime}$.
Then we define the new functions f' and $\tilde{f}{^\prime}$ and check their properties.
Finally we prove (compl ($\tilde{X}{^\prime}$), compl ($\tilde{Y}{^\prime}$))∈R.

With proposition [*] we show $\tilde{Y}{^\prime}$∈$\it Conf\/$($\it ref\/$($\cal {F}$)):
-  pr($\tilde{Y}{^\prime}$) = f (pr($\tilde{X}{^\prime}$)) = f (pr($\tilde{X}$)) = pr($\tilde{Y}$)∈$\it Conf\/$($\cal {F}$), since $\tilde{Y}$∈$\it Conf\/$($\it ref\/$($\cal {F}$));
-  ∀d∈pr($\tilde{Y}{^\prime}$): Yd' = Xf-1(d)'∈$\it Conf\/$($\it ref\/$(l$\scriptstyle \cal {E}$(f-1(d )))) - {∅} = $\it Conf\/$($\it ref\/$(l$\scriptstyle \cal {F}$(d ))) - {∅}, since $\tilde{X}{^\prime}$∈$\it Conf\/$($\it ref\/$($\cal {E}$));
-  busy($\tilde{Y}{^\prime}$) = pr($\tilde{Y}{^\prime}$) - compl ($\tilde{Y}{^\prime}$)⊆pr($\tilde{Y}$) - compl ($\tilde{Y}$)⊆max(pr($\tilde{Y}$)) = max(pr($\tilde{Y}{^\prime}$)), since pr($\tilde{Y}$) = pr($\tilde{Y}{^\prime}$) and compl ($\tilde{Y}$)⊆compl ($\tilde{Y}{^\prime}$).

Thus $\tilde{Y}{^\prime}$ is a configuration of $\it ref\/$($\cal {F}$).
Since l$\scriptstyle \it ref\/$($\scriptstyle \cal {F}$)((f (eo), e*)) = l$\scriptstyle \it ref\/$(b)(e*) = a we have $\tilde{Y}$$\buildrel$a$\over$→$\tilde{Y}{^\prime}$.

Let f' : = f and $\tilde{f}{^\prime}$ : = $\tilde{f}$∪{((eo, e*),(f (eo), e*))}. The new function $\tilde{f}{^\prime}$ is bijective, since the events (eo, e*) and (f (eo), e*) do not occur in the domain and the range of $\tilde{f}$, respectively. By construction f' and $\tilde{f}{^\prime}$ have the required properties.

In order to establish ($\tilde{X}{^\prime}$,$\tilde{Y}{^\prime}$)∈$\tilde{R}$ we still have to show (compl ($\tilde{X}{^\prime}$), compl ($\tilde{Y}{^\prime}$))∈R.
Again we have two cases:

1.1. compl ($\tilde{X}{^\prime}$) = compl ($\tilde{X}$).

Using the properties of $\tilde{f}{^\prime}$, compl ($\tilde{Y}{^\prime}$) = f'(compl ($\tilde{X}{^\prime}$)) = f (compl ($\tilde{X}$)) = compl ($\tilde{Y}$), hence (compl ($\tilde{X}{^\prime}$), compl ($\tilde{Y}{^\prime}$))∈R.
1.2. compl ($\tilde{X}{^\prime}$)≠compl ($\tilde{X}$).

Then compl ($\tilde{X}{^\prime}$) = compl ($\tilde{X}$)∪{eo} and compl ($\tilde{X}$)$\buildrel$b$\over$→compl ($\tilde{X}{^\prime}$).

Since (compl ($\tilde{X}$), compl ($\tilde{Y}$))∈R there is a Y'∈$\it Conf\/$($\cal {F}$) with compl ($\tilde{Y}$) $\buildrel$b$\over$→ Y' and (compl ($\tilde{X}{^\prime}$), Y')∈R.

Using the properties of $\tilde{f}{^\prime}$, compl ($\tilde{Y}{^\prime}$) = f'(compl ($\tilde{X}{^\prime}$)) = f (compl ($\tilde{X}$)∪{eo}) = compl ($\tilde{Y}$)∪{f (eo)}, hence compl ($\tilde{Y}$)$\buildrel$b$\over$→compl ($\tilde{Y}{^\prime}$).

Since eo∈compl ($\tilde{X}{^\prime}$)⊆pr($\tilde{X}{^\prime}$) = pr($\tilde{X}$), it follows that eo∈pr($\tilde{X}$) - compl ($\tilde{X}$) and with lemma [*] b = l$\scriptstyle \cal {E}$(eo) $\not\in$Crit$\scriptstyle \cal {E}$. Hence Y' = compl ($\tilde{Y}{^\prime}$) with lemma [*].

Thus (compl ($\tilde{X}{^\prime}$), compl ($\tilde{Y}{^\prime}$))∈R, which had to be proved.



2. pr($\tilde{X}{^\prime}$)≠pr($\tilde{X}$).

The proof of the second case is similar to that of the first case. However the construction of $\tilde{Y}{^\prime}$ is more complicated since we cannot just use the function f. We need to describe the events by which f is extended.

pr($\tilde{X}{^\prime}$) = pr($\tilde{X}$)∪{eo} and l$\scriptstyle \cal {E}$(eo) = b.

compl ($\tilde{X}{^\prime}$) = $\left\{\vphantom{ \begin{array}{ll}compl(\tilde X) \cup \{e^{\mbox{\scriptsize ... ...of } {\it ref\/}(b) \\ compl(\tilde X) & \mbox{otherwise} \end{array} }\right.$$\begin{array}{ll}compl(\tilde X) \cup \{e^{\mbox{\scriptsize o}}\} & \mbox{if }... ...guration of } {\it ref\/}(b) \\ compl(\tilde X) & \mbox{otherwise} \end{array}$

Thus compl ($\tilde{X}{^\prime}$)⊆compl ($\tilde{X}$)∪{eo}⊆pr($\tilde{X}$)∪{eo} = pr($\tilde{X}{^\prime}$).
With lemma [*] it follows that compl ($\tilde{X}$)∪{eo}∈$\it Conf\/$($\cal {E}$).
Hence compl ($\tilde{X}$) $\buildrel$b$\over$→ compl ($\tilde{X}$) ∪ {eo}.
Since (compl ($\tilde{X}$), compl ($\tilde{Y}$))∈R, there is a do∈E$\scriptstyle \cal {F}$ with compl ($\tilde{Y}$)$\buildrel$b$\over$→compl ($\tilde{Y}$)∪{do}, l$\scriptstyle \cal {F}$(do) = b and (compl ($\tilde{X}$)∪{eo}, compl ($\tilde{Y}$)∪{do})∈R.

We now extend the bijection f by (eo, do).
For this we verify that do is not in the range of f:
Suppose do∈pr($\tilde{Y}$). Since do $\not\in$compl ($\tilde{Y}$), f-1(do)∈pr($\tilde{X}$) - compl ($\tilde{X}$). Thus compl ($\tilde{X}$)∪{f-1(do)}∈$\it Conf\/$($\cal {E}$) with lemma [*] and compl ($\tilde{X}$)$\buildrel$b$\over$→ compl ($\tilde{X}$)∪{f-1(do)}.
Hence b $\not\in$Crit$\scriptstyle \cal {E}$ with lemma [*] and then eo = f-1(do) with lemma [*].
Thus eo∈pr($\tilde{X}$) which contradicts pr($\tilde{X}{^\prime}$)≠pr($\tilde{X}$). So do $\not\in$pr($\tilde{Y}$).

Now we can define $\tilde{Y}{^\prime}$, f' and $\tilde{f}{^\prime}$.
Let f' : = f∪(eo, do) and $\tilde{Y}{^\prime}$ : = {(f'(e), e') | (e, e')∈$\tilde{X}{^\prime}$} = $\tilde{Y}$∪{(do, e*)}.

Using proposition [*] we proof $\tilde{Y}{^\prime}$∈$\it Conf\/$($\it ref\/$($\cal {F}$)):
-  pr($\tilde{Y}{^\prime}$) = pr($\tilde{Y}$)∪{do}∈$\it Conf\/$($\cal {F}$) with lemma [*];
-  ∀d∈pr($\tilde{Y}{^\prime}$): Yd' = Xf'-1(d)'∈$\it Conf\/$($\it ref\/$(l$\scriptstyle \cal {E}$(f'-1(d )))) - {∅} = $\it Conf\/$($\it ref\/$(l$\scriptstyle \cal {F}$(d ))) - {∅};
-  busy($\tilde{Y}{^\prime}$) = pr($\tilde{Y}{^\prime}$) - compl ($\tilde{Y}{^\prime}$) = pr($\tilde{Y}$)∪{do} - compl ($\tilde{Y}{^\prime}$)⊆
pr($\tilde{Y}$)∪{do} - compl ($\tilde{Y}$), since compl ($\tilde{Y}$)⊆compl ($\tilde{Y}{^\prime}$).
It remains to show that pr($\tilde{Y}$)∪{do} - compl ($\tilde{Y}$)⊆max(pr($\tilde{Y}$)∪{do}).
By proposition [*](iii) pr($\tilde{Y}$) is a prefix of pr($\tilde{Y}$)∪{do}, so do∈max(pr($\tilde{Y}$)∪{do}).
Now suppose d∈pr($\tilde{Y}$) - compl ($\tilde{Y}$), but d $\not\in$max(pr($\tilde{Y}$)∪{do}).
Then d∈max(pr($\tilde{Y}$)) by proposition [*], so d < pr($\scriptstyle \tilde{Y}$)∪{do}do. Since compl ($\tilde{Y}$)∪{do} is a prefix of pr($\tilde{Y}$)∪{do} by proposition [*](iii), we have d∈compl ($\tilde{Y}$), which yields a contradiction.

Thus $\tilde{Y}{^\prime}$ is a configuration of $\it ref\/$($\cal {F}$) and with l$\scriptstyle \it ref\/$($\scriptstyle \cal {F}$)(do, e*) = a we have $\tilde{Y}$ $\buildrel$a$\over$→ $\tilde{Y}{^\prime}$.

The new function f' is bijective, as shown above. The same for $\tilde{f}{^\prime}$   : =   $\tilde{f}$∪{((eo, e*),(do, d*))}. By construction f' and $\tilde{f}{^\prime}$ have the required properties.

Now we show ($\tilde{X}{^\prime}$,$\tilde{Y}{^\prime}$)∈$\tilde{R}$ by proving (compl ($\tilde{X}{^\prime}$), compl ($\tilde{Y}{^\prime}$))∈R.
There are again two cases:

2.1. compl ($\tilde{X}{^\prime}$) = compl ($\tilde{X}$).

By construction of $\tilde{Y}{^\prime}$ (as in part 1.1 of the proof) compl ($\tilde{Y}{^\prime}$) = compl ($\tilde{Y}$) and hence (compl ($\tilde{X}{^\prime}$), compl ($\tilde{Y}{^\prime}$))∈R.

2.2. compl ($\tilde{X}{^\prime}$)≠compl ($\tilde{X}$).

Then compl ($\tilde{X}{^\prime}$) = compl ($\tilde{X}$)∪{eo} and by construction of $\tilde{Y}{^\prime}$, compl ($\tilde{Y}{^\prime}$) =
compl ($\tilde{Y}$)∪{do}. We had already that (compl ($\tilde{X}$)∪{eo}, compl ($\tilde{Y}$))∪{do})∈R, hence (compl ($\tilde{X}{^\prime}$), compl ($\tilde{Y}{^\prime}$))∈R.
Thus $\tilde{R}$ is a bisimulation between $\it ref\/$($\cal {E}$) and $\it ref\/$($\cal {F}$). $\Box$